is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
↳ QTRS
↳ DependencyPairsProof
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
IFAPPEND(l1, l2, false) → TL(l1)
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
APPEND(l1, l2) → IS_EMPTY(l1)
IFAPPEND(l1, l2, false) → HD(l1)
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
IFAPPEND(l1, l2, false) → TL(l1)
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
APPEND(l1, l2) → IS_EMPTY(l1)
IFAPPEND(l1, l2, false) → HD(l1)
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
Used ordering: Polynomial interpretation [25,35]:
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
The value of delta used in the strict ordering is 1/8.
POL(cons(x1, x2)) = 1/2 + (4)x_2
POL(IFAPPEND(x1, x2, x3)) = (5/4)x_1 + (1/2)x_3
POL(APPEND(x1, x2)) = (3/2)x_1
POL(tl(x1)) = (1/4)x_1
POL(true) = 1/4
POL(is_empty(x1)) = (1/2)x_1
POL(false) = 1/4
POL(nil) = 1/2
is_empty(nil) → true
is_empty(cons(x, l)) → false
tl(cons(x, l)) → l
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))